(declare-fun _substvar_58_ () Bool)
(declare-fun _substvar_59_ () Bool)
(declare-fun _substvar_82_ () Bool)
(declare-const v8 Bool)
(declare-const r0 Real)
(declare-const r3 Real)
(declare-const r4 Real)
(declare-const r6 Real)
(declare-const r9 Real)
(assert (or _substvar_82_ v8))
(assert (or (>= 4 r3 0.0) _substvar_59_ _substvar_58_))
(assert (>= 0.0 r0 (/ r9 r6) (- r3) (* 4 r4 r3)))
(assert (distinct 0.0 r6 r0))
(check-sat)
